FDL - Nuprl Lemma : minus_functionality_wrt_le

Nuprl Lemma : minus_functionality_wrt_le

i, j:

. (i

j )

((-i)

(-j))

Definitions t T, P Q, x:A. B(x), False, A, A B, i j ,

Lemmas ge wf, add functionality wrt le